$\forall$${\it es}$:ES, $A$, $V$:Type, $i$:Id, ${\it knd}$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\\[0ex]($\forall$$e$:E.
\\[0ex](loc($e$) = $i$) $\Rightarrow$ (kind($e$) = ${\it knd}$) $\Rightarrow$ ((valtype($e$) $\subseteq$r $V$) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ es{-}trigger(${\it es}$;$i$;${\it knd}$;${\it ds}$;$f$))) $\Rightarrow$ (loc($e$) = $i$))